/*
Copyright 2017 Bjoern Lellman, Marianna Girlando, Nicola Olivetti, Gian Luca Pozzato, Quentin Vitalis. 
This file is part of VINTE. VINTE is free software: you can redistribute it and/or modify it under 
the terms of the GNU General Public License as published by the Free Software Foundation, either version 
3 of the License, or (at your option) any later version. NESCOND is distributed in the hope that it will 
be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR 
A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy 
of the GNU General Public License along with VINTE. If not, see <http://www.gnu.org/licenses/>.
*/


/* Automatic generator of formulas.

To test the performances of VINTE and comparing them with the ones of NESCOND, CondLean and UCK,
run: 

  statistic(GoalVars,KBVars,DimKB,NumGoals,Depth,MSec)

Generated formulas have the form: A_1 ^ A_2 ^ É ^ A_n -> B (in order to be used also by the goal-directed UCK)
GoalVars=KBVars=number of different propositional variables
DimKB=n (i.e. number of conjuncts in the antecedent)
NumGoals= number of different Bs to use in the consequent
Depth=maximun level of nesting of formulas
MSec=timeout.

*/

:- op(400,fy,-), 
   op(500,xfy,&), 
   op(600,xfy,v), 
   op(800,xfy,<=>),
   op(400,fy,box), 
   op(400,fy,dia),
   op(400,fy,neg), 
   op(500,xfy,and), 
   op(600,xfy,or),
   op(700,xfy,->), 
   op(700,xfy,=>),
   op(400,xfy,^),
   op(600,xfy,?),
   op(700,xfy,<).
   
:-use_module(library(random)).
:-use_module(library(lists)).
:-use_module(library(timeout)).
:-use_module(library(ordsets)).

genD(ATM,Var,0):-!,length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genD(ATM,Fml,Depth):-random(1,4,Rand),Depth1 is Depth - 1,genDIn(ATM,Rand,Fml,Depth1).
genDIn(ATM,1,true -> Var,_):-length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genDIn(ATM,2,(G) -> (Var),Depth):-length(ATM,L),L1 is L+1,random(1,L1,Position),
  nth(Position,ATM,Var),genG(ATM,G,Depth).
genDIn(ATM,3,(A) => (D),Depth):-genA(ATM,A,Depth),genD(ATM,D,Depth).

genG(ATM,Var,0):-!,length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genG(ATM,Fml,Depth):-random(1,6,Rand),Depth1 is Depth - 1,genGIn(ATM,Rand,Fml,Depth1).
genGIn(ATM,1,Var,_):-length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genGIn(_,2,true,_).
genGIn(ATM,3,(G1) and (G2),Depth):-genG(ATM,G1,Depth),genG(ATM,G2,Depth).
genGIn(ATM,4,(G1) or (G2),Depth):-genG(ATM,G1,Depth),genG(ATM,G2,Depth).
genGIn(ATM,5,(A) => (G),Depth):-genA(ATM,A,Depth),genG(ATM,G,Depth).


genA(ATM,Var,0):-!,length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genA(ATM,Fml,Depth):-random(1,4,Rand),Depth1 is Depth - 1,genAIn(ATM,Rand,Fml,Depth1).
genAIn(ATM,1,Var,_):-length(ATM,L),L1 is L+1,random(1,L1,Position),nth(Position,ATM,Var).
genAIn(ATM,2,(A1) and (A2),Depth):-genA(ATM,A1,Depth),genA(ATM,A2,Depth).
genAIn(ATM,3,(A1) or (A2),Depth):-genA(ATM,A1,Depth),genA(ATM,A2,Depth).


generateKnowledgeBase(0,_,[],_):-!.
generateKnowledgeBase(Dim,ATM,[[x,Fml]|KB],Depth):-genD(ATM,Fml,Depth),                                   
			           Dim1 is Dim-1,
                 generateKnowledgeBase(Dim1,ATM,KB,Depth).
      
     
generatePropVars(1,[p]):-!.                                   
generatePropVars(2,[p,q]):-!.                                   
generatePropVars(3,[p,q,r]):-!.                                   
generatePropVars(4,[p,q,r,p1]):-!.                                   
generatePropVars(5,[p,q,r,p1,q1]):-!.                                   
generatePropVars(6,[p,q,r,p1,q1,r1]):-!.                                   
generatePropVars(7,[p,q,r,p1,q1,r1,p2]):-!.                                   
generatePropVars(8,[p,q,r,p1,q1,r1,p2,q2]):-!.                                   
generatePropVars(9,[p,q,r,p1,q1,r1,p2,q2,r2]):-!.     

/* Where are they now? */
subset(_,0,[]):-!.
subset([H|Tail],N,[H|ResTail]):-N1 is N-1,subset(Tail,N1,ResTail).                              
nth(1,[Head|_],Head):-!.
nth(N,[_|Tail],Res):-N1 is N-1,nth(N1,Tail,Res).


statistic(GoalVars,KBVars,DimKB,NumGoals,Depth,MSec):-
  retractall(successes(_)),
  retractall(timeouts(_)),
  retractall(succLean(_)),
  retractall(timeLean(_)),
  retractall(succNS(_)),
  retractall(timeNS(_)),
  retractall(succVINTE(_)),
  retractall(toVINTE(_)),
  asserta(successes(0)),
  asserta(timeouts(0)),
  asserta(succLean(0)),
  asserta(timeLean(0)),
  asserta(succNS(0)),
  asserta(timeNS(0)),
  asserta(succVINTE(0)),
  asserta(toVINTE(0)),
  generatePropVars(KBVars,ATM),
  subset(ATM,GoalVars,GoalATM),
  generateKnowledgeBase(DimKB,ATM,KB,Depth),
  listOfGoals(GoalATM,Goals,NumGoals,Depth),
/*  write('KB: '),
  write(KB),
  write('\nGOALS: '),
  write(Goals),
  write('\n'),  */
  write('Executing UCK...'),
  executeUCK(KB,Goals,MSec),
  write('DONE\n'),
  successes(N),
  timeouts(T),
  F is NumGoals-N-T,
  write('Executing CondLean...'),
  executeCondLean(KB,Goals,MSec),
  write('DONE\n'),
  succLean(NL),
  timeLean(TL),
  FL is NumGoals-NL-TL,
  createNestedSequent(KB,NS),
  write('Executing NESCOND...'),
  executeNested(NS,Goals,MSec),
  write('DONE\n'),
  succNS(NNS),
  timeNS(TNS),
  FNS is NumGoals-NNS-TNS,
  write('Executing VINTE...'),
  convertNS(KB,KBVINTE),
  convertNS(Goals,GoalsVINTE),
  executeVINTE(KBVINTE,GoalsVINTE,MSec),
  write('DONE\n'),
  succVINTE(SuccVINTE),
  toVINTE(TimeoutsVINTE),
  DiffVINTE is NumGoals-SuccVINTE-TimeoutsVINTE,
  write('Number of timeouts \n'),
  write('UCK                  '),write(T),write('\n'),
  write('CondLean             '),write(TL),write('\n'),
  write('NESCOND              '),write(TNS),write('\n'),
  write('VINTE                '),write(TimeoutsVINTE),write('\n').


convertNS(List,List):-!.
  
listOfGoals(_,[],0,_):-!.
listOfGoals(ATM,[Goal|Tail],N,Depth):-genG(ATM,Goal,Depth),N1 is N-1,listOfGoals(ATM,Tail,N1,Depth).

executeUCK(_,[],_):-!.
executeUCK(KB,[Goal|Tail],MSec):-
  (
  time_out(proveU([x,Goal],KB,[],[x]),MSec,Result),!,
  (
    (
    Result=success,!,
    successes(N),retractall(successes(_)),N1 is N+1,asserta(successes(N1)),
    executeUCK(KB,Tail,MSec)
    );
    (
    timeouts(T),retractall(timeouts(_)),T1 is T+1,asserta(timeouts(T1)),
    executeUCK(KB,Tail,MSec)
    )
  )
  )
  ;
  executeUCK(KB,Tail,MSec).

executeCondLean(_,[],_):-!.
executeCondLean(KB,[Goal|Tail],MSec):-
  (
  time_out(
    (
      struttura(KB,LitSigma,TransSigma,LabSigma),
      struttura([[x,Goal]],LitDelta,TransDelta,LabDelta),
      proveCondLean([LitSigma,TransSigma,LabSigma],[LitDelta,TransDelta,LabDelta],[x])
    ),MSec,Result),!,
  (
    (
    Result=success,!,
    succLean(N),retractall(succLean(_)),N1 is N+1,asserta(succLean(N1)),
    executeCondLean(KB,Tail,MSec)
    );
    (
    timeLean(T),retractall(timeLean(_)),T1 is T+1,asserta(timeLean(T1)),
    executeCondLean(KB,Tail,MSec)
    )
  )
  )
  ;
  executeCondLean(KB,Tail,MSec). 


executeNested(_,[],_):-!.
executeNested(Fml,[Goal|Tail],MSec):-
  (
  time_out(
    (
      proveNS([Fml -> Goal])
    ),MSec,Result),!,
  (
    (
    Result=success,!,
    succNS(N),retractall(succNS(_)),N1 is N+1,asserta(succNS(N1)),
    executeNested(Fml,Tail,MSec)
    );
    (
    timeNS(T),retractall(timeNS(_)),T1 is T+1,asserta(timeNS(T1)),
    executeNested(Fml,Tail,MSec)
    )
  )
  )
  ;
/*  write('Fallimento su '),
  write(Fml -> Goal),
  write('\n'),*/
  executeNested(Fml,Tail,MSec). 


executeVINTE(_,[],_):-!.
executeVINTE(Fml,[Goal|Tail],MSec):-
  (
  time_out(
    (
      proveVINTE([[Fml],[Goal]],_)
    ),MSec,Result),!,
  (
    (
    Result=success,!,
    succVINTE(N),retractall(succVINTE(_)),N1 is N+1,asserta(succVINTE(N1)),
    executeVINTE(Fml,Tail,MSec)
    );
    (
    toVINTE(T),retractall(toVINTE(_)),T1 is T+1,asserta(toVINTE(T1)),
    executeVINTE(Fml,Tail,MSec)
    )
  )
  )
  ;
  executeVINTE(Fml,Tail,MSec). 



/* ---------------------------------------------------------------- */
/* ---------------------------------------------------------------- */

/* The following predicates implement UCK 1.0 */

/* ---------------------------------------------------------------- */
/* ---------------------------------------------------------------- */

proveU([_,true],_,_,_):-!.
proveU([X,Q],Gamma,_,_):-atom(Q),member([X,Q],Gamma),!.

/* Rules */
proveU([X,G1 and G2],Gamma,Trans,Labels):-
  proveU([X,G1],Gamma,Trans,Labels),!,
  proveU([X,G2],Gamma,Trans,Labels).
  
proveU([X,G1 or G2],Gamma,Trans,Labels):-
  (proveU([X,G1],Gamma,Trans,Labels),!);proveU([X,G2],Gamma,Trans,Labels).
  
proveU([X,A => G],Gamma,Trans,Labels):-  
  generaLabels(Y,Labels),
  proveU([Y,G],Gamma,[[X,A,Y]|Trans],[Y|Labels]).
  
proveU([X,A,Y],_,Trans,_):-
  member([X,AP,Y],Trans),
  flat(A,DefA),
  flat(AP,DefAP),
  proveU([x,A],DefAP,[],[x]),
  proveU([x,AP],DefA,[],[x]).
  
proveU([X,Q],Gamma,Trans,Labels):-
  member([X,G->Q],Gamma),
  atom(Q),
  proveU([X,G],Gamma,Trans,Labels).

proveU([X,Q],Gamma,Trans,Labels):-
  member([Y,F=>(G->Q)],Gamma),
  atom(Q),
  proveU([X,G],Gamma,Trans,Labels),
  extract(F,List),
  proveList(X,Y,List,Gamma,Trans,Labels).


/* Predicate implementing the flattening of a conjunction of formulas */
flat(P,[[x,P]]):-atom(P),!.
flat(A1 and A2,Res):-flat(A1,FlatA1),flat(A2,FlatA2),append(FlatA1,FlatA2,Res).

/* Auxiliary predicates to compute Uprop */
extract(Rest=>A,[A|Tail]):-!,extract(Rest,Tail).
extract(F,[F]):-!.
proveList(K,Y,[A],Gamma,Trans,Labels):-
  proveU([Y,A,K],Gamma,Trans,Labels).
proveList(X,Y,[A|Tail],Gamma,Trans,Labels):-
  proveU([K,A,X],Gamma,Trans,Labels),
  proveList(K,Y,Tail,Gamma,Trans,Labels).


/* -------------------------------------------------------------- */

/* This predicate generates a "new" label for that branch */
generaLabels(x,Labels):-true,\+member(x,Labels),!.
generaLabels(y,Labels):-true,\+member(y,Labels),!.
generaLabels(z,Labels):-true,\+member(z,Labels),!.
generaLabels(u,Labels):-true,\+member(z,Labels),!.
generaLabels(v,Labels):-true,\+member(z,Labels),!.
generaLabels(w,Labels):-true,\+member(z,Labels),!.
generaLabels(k,Labels):-true,\+member(k,Labels),!.
generaLabels(j,Labels):-true,\+member(j,Labels),!.
generaLabels(i,Labels):-true,\+member(i,Labels),!.
generaLabels(x+1,[i|_]):-!.
generaLabels(x+N1,[Last|_]):-Last=x+N,N1 is N+1,!.



/* ---------------------------------------------------------------- */
/* ---------------------------------------------------------------- */

/* The following predicates implement CondLean 3.1 */

/* ---------------------------------------------------------------- */
/* ---------------------------------------------------------------- */

/* Axioms */
/* true and false */
proveCondLean([LitSigma,_,_],_,_):-
  member([_,false],LitSigma),!.
proveCondLean(_,[LitDelta,_,_],_):-
  member([_,true],LitDelta),!.
proveCondLean([LitSigma,_,_],[LitDelta,_,_],_):-
  member(F,LitSigma),member(F,LitDelta),!.
proveCondLean([_,TransSigma,_],[_,TransDelta,_],_):-
  member(F,TransSigma),member(F,TransDelta),!.
proveCondLean([_,_,ComplexSigma],[_,_,ComplexDelta],_):-
  member(F,ComplexSigma),member(F,ComplexDelta),!.

/* Rules */
/* and L */
proveCondLean([LitSigma,TransSigma,ComplexSigma],Delta,Labels):-
  select([X,A and B],ComplexSigma,ResComplexSigma),!,
  put([X,A],LitSigma,ResComplexSigma,TempLitSigma,TempComplexSigma),
  put([X,B],TempLitSigma,TempComplexSigma,NewLitSigma,NewComplexSigma),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],Delta,Labels).
/* or R */
proveCondLean(Sigma,[LitDelta,TransDelta,ComplexDelta],Labels):-
  select([X,A or B],ComplexDelta,ResComplexDelta),!,
  put([X,A],LitDelta,ResComplexDelta,TempLitDelta,TempComplexDelta),
  put([X,B],TempLitDelta,TempComplexDelta,NewLitDelta,NewComplexDelta),
  proveCondLean(Sigma,[NewLitDelta,TransDelta,NewComplexDelta],Labels).
/* neg R */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],
    Labels):-
  select([X,neg A],ComplexDelta,ResComplexDelta),!,
  put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ResComplexDelta],Labels).
/* neg L */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels)
  :-select([X,neg A],ComplexSigma,ResComplexSigma),!,
  put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
  proveCondLean([LitSigma,TransSigma,ResComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Labels).
/* -> R */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels)
  :-select([X,A -> B],ComplexDelta,ResComplexDelta),!,
  put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
  put([X,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Labels).
/* => R */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels)
  :-select([X,A => B],ComplexDelta,ResComplexDelta),!,
  generaLabels(Y,Labels),
  put([Y,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta),
  proveCondLean([LitSigma,[[X,A,Y]|TransSigma],ComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],
    [Y|Labels]).
/* and R */
proveCondLean(Sigma,[LitDelta,TransDelta,ComplexDelta],Labels):-
  select([X,A and B],ComplexDelta,ResComplexDelta),!,
  put([X,A],LitDelta,ResComplexDelta,FirstLitDelta,FirstComplexDelta),
  put([X,B],LitDelta,ResComplexDelta,SecLitDelta,SecComplexDelta),
  proveCondLean(Sigma,[FirstLitDelta,TransDelta,FirstComplexDelta],Labels),
  proveCondLean(Sigma,[SecLitDelta,TransDelta,SecComplexDelta],Labels).
/* or L */
proveCondLean([LitSigma,TransSigma,ComplexSigma],Delta,Labels):-
  select([X,A or B],ComplexSigma,ResComplexSigma),!,
  put([X,A],LitSigma,ResComplexSigma,FirstLitSigma,FirstComplexSigma),
  put([X,B],LitSigma,ResComplexSigma,SecLitSigma,SecComplexSigma),
  proveCondLean([FirstLitSigma,TransSigma,FirstComplexSigma],Delta,Labels),
  proveCondLean([SecLitSigma,TransSigma,SecComplexSigma],Delta,Labels).
/* -> L */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels):-
  select([X,A -> B],ComplexSigma,ResComplexSigma),!,
  put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
  put([X,B],LitSigma,ResComplexSigma,NewLitSigma,NewComplexSigma),
  proveCondLean([LitSigma,TransSigma,ResComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Labels),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels).
/* => L  */
proveCondLean([LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Labels):-
  select([X,A => B],ComplexSigma,ResComplexSigma),
  member([X,A_1,Y],TransSigma),
  proveCondLean([[],[[X,A_1,Y]],[]],[[],[[X,A,Y]],[]],Labels),
  put([Y,B],LitSigma,ResComplexSigma,NewLitSigma,NewComplexSigma),
  proveCondLean([NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ComplexDelta],
    Labels).
/* EQ */
proveCondLean([_,TransSigma,_],[_,TransDelta,_],_):-
  member([X,A,Y],TransSigma),member([X,B,Y],TransDelta),
  /* The premises are "independent" from the conclusion, so we can use label x
     for their proofs */
  put([x,A],[],[],FirstLitSigma,FirstComplexSigma),
  put([x,B],[],[],FirstLitDelta,FirstComplexDelta),
  put([x,B],[],[],SecLitSigma,SecComplexSigma),
  put([x,A],[],[],SecLitDelta,SecComplexDelta),
  proveCondLean([FirstLitSigma,[],FirstComplexSigma],[FirstLitDelta,[],FirstComplexDelta],
    [x]),
  proveCondLean([SecLitSigma,[],SecComplexSigma],[SecLitDelta,[],SecComplexDelta],
    [x]).


/* --------------------------------------------------------------------------------------- */


/* This predicate finds all the labels in the sequent 
      etichette(+Sequente,-ListaEtichette) */
etichette([],[]):-!.
etichette([[L,_]|Tail],[L|TailLab]):-etichette(Tail,TailLab),\+member(L,TailLab),!.
etichette([[L,_,L]|Tail],[L|TailLab]):-etichette(Tail,TailLab),\+member(L,TailLab),!.
etichette([[L1,_,L2]|Tail],[L1,L2|TailLab]):-etichette(Tail,TailLab),
  \+member(L1,TailLab),\+member(L2,TailLab),!.
etichette([[L1,_,L2]|Tail],[L1|TailLab]):-etichette(Tail,TailLab),
  \+member(L1,TailLab),member(L2,TailLab),!.
etichette([[L1,_,L2]|Tail],[L2|TailLab]):-etichette(Tail,TailLab),
  \+member(L2,TailLab),member(L1,TailLab),!.
etichette([_|Tail],Labels):-etichette(Tail,Labels).

/* This predicate creates a partition of the sequent in atomic, transition and complex formulas */
struttura([],[],[],[]):-!.
struttura([[X,A and B]|Tail],Literal,Transaction,[[X,A and B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A or B]|Tail],Literal,Transaction,[[X,A or B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A -> B]|Tail],Literal,Transaction,[[X,A -> B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A => B]|Tail],Literal,Transaction,[[X,A => B]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,neg A]|Tail],Literal,Transaction,[[X,neg A]|ForTail]):-
  struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A,Y]|Tail],Literal,[[X,A,Y]|TransTail],Formulae):-
  struttura(Tail,Literal,TransTail,Formulae),!.
struttura([X|Tail],[X|LitTail],Transition,Formulae):-
  struttura(Tail,LitTail,Transition,Formulae),!.

/* This predicate inserts a formula in the correct list; more precisely, a formula
   can be an atomic formula or a complex formula */
put([X,A and B],Literal,Formulae,Literal,[[X,A and B]|Formulae]):-!.
put([X,A or B],Literal,Formulae,Literal,[[X,A or B]|Formulae]):-!.
put([X,A -> B],Literal,Formulae,Literal,[[X,A -> B]|Formulae]):-!.
put([X,A => B],Literal,Formulae,Literal,[[X,A => B]|Formulae]):-!.
put([X,neg A],Literal,Formulae,Literal,[[X,neg A]|Formulae]):-!.
put(X,Literal,Formulae,[X|Literal],Formulae):-!.




/* Nested sequent calculi */
removeLabels([],[]):-!.
removeLabels([[_,Fml]|Tail],[Fml|ResTail]):-removeLabels(Tail,ResTail).
createConj([Singleton],Singleton):-!.
createConj([Head|Tail],Head and FmlTail):-createConj(Tail,FmlTail).
createNestedSequent(KB,Fml):-removeLabels(KB,KBUnlab),createConj(KBUnlab,Fml).


fillTheHole(NS,ListToFill,NewNS):-select(hole,NS,TempNS),!,
								  append(TempNS,ListToFill,NewNS).
fillTheHole(NS,ListToFill,[[[Fml,NewGamma],AppliedConditionals]|TempNS]):-select([[Fml,Gamma],AppliedConditionals],NS,TempNS),
								  fillTheHole(Gamma,ListToFill,NewGamma).

selectList([],NS,[hole|NS]).
selectList([Fml|Tail],NS,NewNS):-select(Fml,NS,TempNS),
								 selectList(Tail,TempNS,NewNS).
						
deepSelect(List,NS,NewNS):-selectList(List,NS,NewNS).
deepSelect(List,NS,[[[Fml,NewGamma],AppliedConditionals]|NewNS]):-select([[Fml,Gamma],AppliedConditionals],NS,NewNS),
						   deepSelect(List,Gamma,NewGamma).

memberList([],_):-!.
memberList([Head|Tail],NS):-member(Head,NS),memberList(Tail,NS).
deepMember(List,NS):-memberList(List,NS),!.
deepMember(List,NS):-member([[_,Gamma],_],NS),
					 deepMember(List,Gamma),!.

/* Axioms closing branches */
proveNS(NS):-deepMember([P,neg P],NS),!.
proveNS(NS):-deepMember([true],NS),!.
proveNS(NS):-deepMember([neg false],NS),!.
/* Rules with one premise */
proveNS(NS):-deepSelect([neg neg A],NS,NewNS),!,fillTheHole(NewNS,[A],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A or B],NS,NewNS),!,fillTheHole(NewNS,[A,B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([neg (A and B)],NS,NewNS),!,fillTheHole(NewNS,[neg A,neg B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A -> B],NS,NewNS),!,fillTheHole(NewNS,[neg A,B],DefNS),proveNS(DefNS).
proveNS(NS):-deepSelect([A => B],NS,NewNS),!,fillTheHole(NewNS,[[[A,[B]],[]]],DefNS),proveNS(DefNS).
/* Rules with two or three premises (introducing a branch in a backward proof search) */
proveNS(NS):-deepSelect([neg (A or B)],NS,NewNS),!,fillTheHole(NewNS,[neg A],NS1),fillTheHole(NewNS,[neg B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-deepSelect([A and B],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-deepSelect([neg (A -> B)],NS,NewNS),!,fillTheHole(NewNS,[A],NS1),fillTheHole(NewNS,[neg B],NS2),proveNS(NS1),proveNS(NS2).
proveNS(NS):-
    deepSelect([neg (A => B),[[C,Delta],AppliedConditionals]],NS,NewNS),
    \+member(neg (A => B),AppliedConditionals),!,
    proveNS([A,neg C]),
    proveNS([C,neg A]),
    fillTheHole(NewNS,[neg(A => B),[[C,[neg B|Delta]],[neg (A => B)|AppliedConditionals]]],DefNS),
    proveNS(DefNS).




/* Internal calculi for logic VW */

/* Axioms closing branches */
prove([Gamma,Delta],tree(axb,[Gamma,Delta],no,no)):-member(false,Gamma),!.
prove([Gamma,Delta],tree(axt,[Gamma,Delta],no,no)):-member(true,Delta),!.
prove([Gamma,Delta],tree(init,[Gamma,Delta],no,no)):-member(P,Gamma),member(P,Delta),!.


/* Rules with one premise */
prove([Gamma,Delta],tree(negL,[Gamma,Delta],SubTree,no)):-
  select(-A,Gamma,NewGamma),\+member(A,Delta),!,prove([NewGamma,[A|Delta]],SubTree).
prove([Gamma,Delta],tree(negR,[Gamma,Delta],SubTree,no)):-
  select(-A,Delta,NewDelta),\+member(A,Gamma),!,prove([[A|Gamma],NewDelta],SubTree).
prove([Gamma,Delta],tree(impR,[Gamma,Delta],SubTree,no)):-
  select(A->B,Delta,NewDelta),(\+member(A,Gamma);\+member(B,NewDelta)),!,prove([[A|Gamma],[B|NewDelta]],SubTree).
prove([Gamma,Delta],tree(andL,[Gamma,Delta],SubTree,no)):-
  select(A^B,Gamma,NewGamma),(\+member(A,NewGamma);\+member(B,NewGamma)),!,prove([[A,B|NewGamma],Delta],SubTree).
prove([Gamma,Delta],tree(orR,[Gamma,Delta],SubTree,no)):-
  select(A ? B,Delta,NewDelta),(\+member(A,NewDelta);\+member(B,NewDelta)),!,prove([Gamma,[A,B|NewDelta]],SubTree).
prove([Gamma,Delta],tree(n,[Gamma,Delta],SubTree,no)):-
  \+memberOrdSet([[false],true],Delta),Gamma \== [true],Delta \== [false],!,prove([Gamma,[[[false],true]|Delta]],SubTree).
prove([Gamma,Delta],tree(precR,[Gamma,Delta],SubTree,no)):-
  select(A < B,Delta,NewDelta),\+memberOrdSet([[A],B],Delta),!,prove([Gamma,[[[A],B]|NewDelta]],SubTree).
prove([Gamma,Delta],tree(w,[Gamma,Delta],SubTree,no)):-
  member([Sigma,_],Delta),
  \+is_list_in(Sigma,Delta),
  !,
  append(Delta,Sigma,NewDelta),
  prove([Gamma,NewDelta],SubTree).
prove([Gamma,Delta],tree(condR,[Gamma,Delta],SubTree,no)):-
  select(A=>B,Delta,NewDelta),
  (\+member((A^(-B)) < A,Gamma);\+memberOrdSet([[false],A],NewDelta)),
  !,
  prove([[(A^(-B)) < A|Gamma],[[[false],A]|NewDelta]],SubTree).  

/* Rules with two premises */
prove([Gamma,Delta],tree(impL,[Gamma,Delta],Sub1,Sub2)):-
  select(A->B,Gamma,NewGamma),\+member(B,NewGamma),\+member(A,Delta),!,prove([[B|NewGamma],Delta],Sub1),prove([NewGamma,[A|Delta]],Sub2).
prove([Gamma,Delta],tree(andR,[Gamma,Delta],Sub1,Sub2)):-
  select(A^B,Delta,NewDelta),\+member(A,NewDelta),\+member(B,NewDelta),!,prove([Gamma,[A|NewDelta]],Sub1),prove([Gamma,[B|NewDelta]],Sub2).
prove([Gamma,Delta],tree(orL,[Gamma,Delta],Sub1,Sub2)):-
  select(A ? B,Gamma,NewGamma),\+member(A,NewGamma),\+member(B,NewGamma),!,prove([[A|NewGamma],Delta],Sub1),prove([[B|NewGamma],Delta],Sub2).
prove([Gamma,Delta],tree(condL,[Gamma,Delta],Sub1,Sub2)):-
  select(A => B,Gamma,NewGamma),
  \+member(false < A,NewGamma),\+memberOrdSet([[A ^ (-(B))],A],Delta),!,
  prove([[false < A|NewGamma],Delta],Sub1),
  prove([NewGamma,[[[A^(-B)],A]|Delta]],Sub2).
prove([Gamma,Delta],tree(t,[Gamma,Delta],Sub1,Sub2)):-
  member(A < B,Gamma),
  \+member(B,Delta),
  \+memberOrdSet([[false],A],Delta),
  !,
  prove([Gamma,[B|Delta]],Sub1),
  prove([Gamma,[[[false],A]|Delta]],Sub2).
prove([Gamma,Delta],tree(com,[Gamma,Delta],Sub1,Sub2)):-
  select([Sigma1,A],Delta,Temp),
  select([Sigma2,B],Temp,NewDelta),
  append(Sigma1,Sigma2,NewSigma),
  remove_duplicates(NewSigma,SigmaDef),
  \+memberOrdSet([SigmaDef,A],Delta),
  \+memberOrdSet([SigmaDef,B],Delta),
  !,
  prove([Gamma,[[SigmaDef,A],[Sigma2,B]|NewDelta]],Sub1),
  prove([Gamma,[[SigmaDef,B],[Sigma1,A]|NewDelta]],Sub2).
prove([Gamma,Delta],tree(precL,[Gamma,Delta],Sub1,Sub2)):-
  member(A < B,Gamma),select([Sigma,C],Delta,NewDelta),
  remove_duplicates([B|Sigma],NewSigma),
  \+memberOrdSet([NewSigma,C],Delta),
  \+memberOrdSet([Sigma,A],Delta),!,
  prove([Gamma,[[NewSigma,C]|NewDelta]],Sub1),
  prove([Gamma,[[Sigma,A]|Delta]],Sub2).

/* Jump rule */
prove([Gamma,Delta],tree(jump,[Gamma,Delta],SubTree,no)):-member([Sigma,A],Delta),prove([[A],Sigma],SubTree).



% memberOrdSet([Sigma,A],Delta)
% It succeeds if and only if Delta contains a block [Psi,A] such that Sigma \subseteq Psi - To this aim, ordsets are used to compare sets corresponding to lists of formulas
memberOrdSet([Sigma,A],Delta):-
list_to_ord_set(Sigma,SigmaOrdSet),
member([Psi,A],Delta),
list_to_ord_set(Psi,PsiOrdSet),
%ord_seteq(SigmaOrdSet,PsiOrdSet).
ord_subset(SigmaOrdSet,PsiOrdSet).



% It removes duplicated items in the list
remove_duplicates([],[]):-!.
remove_duplicates([Head|Tail],NewTail):-member(Head,Tail),!,remove_duplicates(Tail,NewTail).
remove_duplicates([Head|Tail],[Head|NewTail]):-remove_duplicates(Tail,NewTail).


% It checks whether a list L is included into anothe list LP
is_list_in(L,LP):-list_to_ord_set(L,OL),list_to_ord_set(LP,OLP),ord_subset(OL,OLP).
